Nuprl Lemma : ma-abs-interface-loc 11,40
A:Type, X:MaInterface(A), es:ES.
ma-interface-consistent(es;X)  (e:E. ((e  [[X]]))  (loc(e)  ma-interface-locs(X))) 
latex

Definitionsb, can-apply(f;x), e  X, [[X]], Id, (x  l), P  Q, E, x:A. B(x), ma-interface-consistent(es;X), ES, MaInterface(T), Type, False, t  T, ff, isl(x), , x:AB(x), s = t, A, x:A  B(x), P & Q, P  Q, Unit, left + right, ma-in-interface(es;X;e)
Lemmasma-in-interface-loc, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, assert wf, false wf

origin